Require Import Omega.
Require Import Arith.
Require Import Classical.

Ltac elim_clear H := elim H;intros;clear H.
Ltac g_intro H := generalize H;intros.

Definition Cycle := nat.
Definition Time := nat.

Definition Var := Cycle -> Prop.

Variables t1_PT : Time.
Hypothesis t1_LargerThan0 : 
    1 <= t1_PT.
    
(*help functions*)
Definition being_true (v:Var) c1 c2 :=
                    forall c, c1 <= c <= c2 -> v c.
Definition being_false (v:Var) c1 c2 :=
                    forall c, c1 <= c <= c2 -> ~ v c.
                
Theorem Induction_lt: 
            forall P : nat -> Prop,
       (forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
       forall n : nat, P n.
intros.
 eapply well_founded_induction_type.
   cut (well_founded lt).
    intros.
    apply H0.
   apply Wf_nat.lt_wf.
  auto.       
Qed.

(*a map from cycle to real time*)
Variable f : Cycle -> Time.
Hypothesis f_monotonic : forall c, f c < f (S c).

Lemma f_all_lg_0 : forall c, 0 < f (S c).
intros.
cut (f 0 < f (S c)).
  omega.
induction c.
 apply f_monotonic.
generalize (f_monotonic (S c)); intros;  omega.
Qed.

Lemma f_1 :
    forall c1 c2, c1 < c2 -> f c1 < f c2.
intros.
induction H.
  eapply f_monotonic.
cut (f m < f (S m)); intros.
  omega.
 eapply f_monotonic.
Qed.

Lemma f_1_le :
    forall c1 c2, c1 <= c2 -> f c1 <= f c2.
intros.
elim H; auto.
intros.
cut (f m < f (S m)); intros; try  omega.
apply f_1; auto.
Qed.

Lemma f_2 :
    forall c1 c2, f c1 < f c2 -> c1 < c2.
induction c1; induction c2; intros; try  omega.
   cut (f 0 < f (S c1)).
  intros.
     omega.
 clear H IHc1.
   apply f_1;  omega.
cut (c1 < c2 \/ c1 = c2 \/ c2 < c1); intros; try  omega.
  elim H0; intros.
  omega.
elim H1.
 intros.
   rewrite H2 in H.
    omega.
intros.
  cut (S c2 < S c1).
 intros.
   generalize (f_1 (S c2) (S c1)); intros.
    omega.
 omega.
Qed.
    
Lemma f_3_inner_leftfix:
        forall c1 c2 c3 v, c1 <= c2 <= c3 -> f c3 - f c1 < v -> f c2 - f c1 < v.
intros.
elim_clear H.
g_intro (f_1_le c2 c3 H2).
omega.
Qed.

Lemma f_3_inner_rightfix:
        forall c1 c2 c3 v, c1 <= c2 <= c3 -> f c3 - f c1 < v -> f c3 - f c2 < v.
intros.
elim_clear H.
g_intro (f_1_le c1 c2 H1).
omega.
Qed.

Lemma f_3_inner:
    forall c1 c2 c3 c4 v, c1<=c2 -> c2<=c3 -> c3 <= c4->
                f c4 - f c1 < v -> f c3 - f c2 < v.
intros.
g_intro (f_1_le c1 c2 H).
g_intro (f_1_le c3 c4 H1).
omega.
Qed.
    
Hypothesis f_TimerLargerThanCycleInterval :
                    forall c, f (S c) -  f c < t1_PT.  

(*
all the relays without timer
i0 - start
i1 - reset
i2 - player 1
i3 - player 2
i4 - player 3

m1 - running symbol
m2 - player 1
m3 - player 2
m4 - player 3
m5 - lock symbol if any one press the button

o0 - time out
o1 - player 1 pressed
o2 - player 2 pressed
o3 - player 3 pressed

*)
Variables i0 i1 i2 i3 i4 : Var.
Variables m1 m2 m3 m4 m5: Var.
Variables o0 o1 o2 o3 : Var.


(*the model of timer*)
Variable t1 : Var.

Axiom h_t1_reset : forall c, ~ m1 c -> ~ t1 c. 

Axiom h_t1_set : 
        forall c1 c2, t1_PT <= f (pred c2) - f (pred c1) -> 
            being_true m1 c1 c2 -> t1 c2. 
            
Axiom h_t1_true :
        forall c2, t1 c2 -> exists c1, t1_PT <= f (pred c2) - f (pred c1) /\ being_true m1 c1 c2.

(*predicates about the struct of the PLC*)

Hypothesis h_m1 : forall c, m1 c = 
                                            ((i0 c \/ m1 (pred c)) 
                                            /\ ~ i1 c).
 
Hypothesis h_m2 : forall c, m2 c = 
                                            (((~ t1 c /\ i2 c /\ ~ m5 (pred c)) 
                                            \/ m2 (pred c)) 
                                            /\ m1 c).

Hypothesis h_m3 : forall c, m3 c = 
                                            (((~ t1 c /\ i3 c /\ ~ m5 (pred c)) 
                                            \/ m3 (pred c)) 
                                            /\ m1 c).
                                            
Hypothesis h_m4 : forall c, m4 c = 
                                            (((~ t1 c /\ i4 c /\ ~ m5 (pred c)) 
                                            \/ m4 (pred c)) 
                                            /\ m1 c).
                                                                                        
Hypothesis h_m5 : forall c, m5 c =
                                            (((m2 c \/ m3 c \/ m4 c) 
                                            \/ m5 (pred c)) 
                                            /\ m1 c).

Hypothesis h_o1 : forall c, o1 c = m2 c.
                                            
Hypothesis h_o2 : forall c, o2 c = m3 c.

Hypothesis h_o3 : forall c, o3 c = m4 c.

Hypothesis h_o0 : forall c, o0 c = 
                                            (t1 c /\ ~ m5 c).

(*properties*)



Lemma reset_no_start_m1 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        being_false m1 c1 c2. 
intros.
intro.
intro.
elim H1.
intro.
clear H1.
elim H2.
 intros.
   red in |- *; intros.
   generalize (h_m1 c1); intros.
   rewrite H4 in H3; intros.
   elim H3; auto.
intros.
  red in |- *; intros.
  generalize (h_m1 (S m)); intros.
  rewrite H6 in H5; intros.
  elim H5; intros.
  simpl in H7.
  elim H7; intros.
 red in H0.
   generalize (H0 (S m)); intros.
   elim H10.
   omega.
 auto.
apply H3.
 auto.
    omega.
auto.
Qed.    

Lemma reset_no_start_m2 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m2 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m2 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.        
    
Lemma reset_no_start_m3 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m3 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m3 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.            
        
Lemma reset_no_start_m4 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m4 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m4 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.            

Lemma reset_no_start_m5 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 -> 
        being_false m5 c1 c2.
intros.
intro; intros.
generalize reset_no_start_m1; intros.
cut (~ m1 c); intros.
 generalize (h_m5 c); intros.
   rewrite H4 in |- *; intro.
   elim H5; auto.
unfold being_false in H2.
   eapply H2.
   apply H.
  apply H0.
  auto.
Qed.    

Lemma noi2_nom2 : forall c, ~ m2 c -> ~ i2 (S c) -> ~ m2 (S c).
unfold not in |- *; intros.
generalize (h_m2 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma noi3_nom3 : forall c, ~ m3 c -> ~ i3 (S c) -> ~ m3 (S c).
unfold not in |- *; intros.
generalize (h_m3 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma noi4_nom4 : forall c, ~ m4 c -> ~ i4 (S c) -> ~ m4 (S c).
unfold not in |- *; intros.
generalize (h_m4 (S c)); intros.
rewrite H2 in H1; clear H2.
elim_clear H1.
elim_clear H2.
  tauto.
auto.
Qed.

Lemma reset_start_noi2_nom2 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i2 (S c2) c3 -> 
        being_false m2 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m2 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi2_nom2; auto.
intros.
  apply noi2_nom2; auto.
  apply H9.
   omega.
Qed.

Lemma reset_start_noi3_nom3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i3 (S c2) c3 -> 
        being_false m3 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m3 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi3_nom3; auto.
intros.
  apply noi3_nom3; auto.
  apply H9.
   omega.
Qed.

Lemma reset_start_noi4_nom4 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, c2 < c3 -> being_false i4 (S c2) c3 -> 
        being_false m4 (S c2) c3.   
intros.
intro.
intro.
generalize (reset_no_start_m4 c1 c2 H0 H1); intros.
elim H5.
intro.
elim H7.
 intros.
   apply noi4_nom4; auto.
intros.
  apply noi4_nom4; auto.
  apply H9.
   omega.
Qed.

Lemma reset_noi2_nom2 : 
    forall c1 c2, i1 c1 -> being_false i2 c1 c2 ->
        being_false m2 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m2 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m2 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_noi3_nom3 : 
    forall c1 c2, i1 c1 -> being_false i3 c1 c2 ->
        being_false m3 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m3 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m3 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_noi4_nom4 : 
    forall c1 c2, i1 c1 -> being_false i4 c1 c2 ->
        being_false m4 c1 c2.   
intros.
intro.
intro.
elim H1.
intro.
elim H2.
 intros.
   intro.
   generalize (h_m4 c1); intros.
   rewrite H5 in H4.
   elim_clear H4.
   generalize (h_m1 c1); intros.
   rewrite H4 in H7.
   elim_clear H7.
   auto.
intros.
  intro.
  generalize (h_m4 (S m)); intros.
  rewrite H7 in H6.
  elim_clear H6.
  elim_clear H8.
 elim_clear H6.
   elim_clear H10.
   red in H0.
   generalize (H0 (S m)); intros.
   apply H10.
   omega.
 auto.
simpl in H6.
  apply H4; try  omega.
  auto.
Qed.

Lemma reset_start_noreset_m1 :
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
            forall c3, being_false i1 (S c2) c3 ->
                being_true m1 (S c2) c3. 
intros.
intro.
intro.
elim H3.
intro.
elim H4; intros.
 generalize (h_m1 (S c2)); intros.
   rewrite H6 in |- *.
   split.
  auto.
 auto.
generalize (h_m1 (S m)); intros.
  rewrite H8 in |- *.
  split.
 right; simpl in |- *.
   apply H6;  omega.
auto.
Qed.

Lemma reset_start_time_t1_remain_false:
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false t1 (S c2) c3.
intros.
intro.
intros.
red in |- *; intros.
generalize (h_t1_true _ H6); intros.
elim_clear H7.
elim_clear H8.
generalize (reset_no_start_m1 c1 c2 H0 H1); intros.
red in H8; red in H9; red in H8.
generalize (H9 c2); intros.
generalize (H8 c2); intros.
cut (x <= c2 <= c /\ c1 <= c2 <= c2); intros.
 elim H12; auto.
split;auto.
split.
Focus 2.
elim H5;omega.
   cut (x <= c2 \/ c2 < x); intros.
Focus 2.
omega.
    elim H12; intros; auto.
assert (f (pred c) - f (pred x) < t1_PT).
eapply  (f_3_inner c2 (pred x) (pred c) c3 t1_PT).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
try omega.
cut (f (pred x) < f (pred c));intros.
g_intro ( f_2 (pred x) (pred c) H14).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14.
omega.
clear H H0 H1 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
clear H H0 H1 H3 H4 H6 H7 H8 H9 H10 H11 H12 H13.
omega.
auto.
clear H H0 H1 H3 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
Qed.

Lemma reset_start_exceed_time_t1_m5_false_general : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            c2 < c3 ->
            being_false i2 (S c2) c3 ->
            being_false i3 (S c2) c3 ->
            being_false i4 (S c2) c3 ->
            being_false i1 (S c2) c3 ->
            ~ m5 c3.
intro.
intro.
intro.
intro.
intro.
intro.
intro.
intro.
elim H3; intros.
 rewrite (h_m5 (S c2)) in |- *; red in |- *; intros.
   elim_clear H8.
   elim_clear H9.
  elim_clear H8.
   generalize reset_start_noi2_nom2; intros.
     red in H8; red in H8;  eapply (H8 c1 c2); auto.
    elim_clear H9.
   generalize reset_start_noi3_nom3; intros.
     red in H9; red in H9;  eapply (H9 c1 c2); auto.
    generalize reset_start_noi4_nom4; intros.
    red in H9; red in H9;  eapply (H9 c1 c2); auto.
   simpl in *.
   rewrite (h_m5 c2) in H8.
   elim_clear H8.
   generalize reset_no_start_m1; intros.
   red in H8; red in H8;  eapply (H8 c1 c2 H0 H1 c2); auto.
  rewrite (h_m5 (S m)) in |- *; red in |- *; intros.
  elim_clear H10.
  elim_clear H11.
 elim_clear H10.
  generalize reset_start_noi2_nom2; intros.
    red in H10; red in H10;  eapply H10.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < S m); intros.
     apply H13.
     omega.
    auto.
    cut (S c2 <= S m <= S m); try  omega.
    intros.
    apply H13.
    auto.
   elim_clear H11.
  generalize reset_start_noi3_nom3; intros.
    red in H11; red in H11;  eapply H11.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < S m); intros; try  omega.
    apply H13.
    auto.
    cut (S c2 <= S m <= S m); intros; try  omega.
    apply H13.
    auto.
   generalize reset_start_noi4_nom4; intros.
   red in H11; red in H11;  eapply H11.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < S m); intros; try  omega.
   apply H13.
   auto.
   cut (S c2 <= S m <= S m); intros; try  omega.
   apply H13.
   auto.
  simpl in *.
  apply H5; try intro; intros.
 apply H6; try  omega.
apply H7; try  omega.
apply H8; try  omega.
apply H9; try  omega.
auto.
Qed.

Lemma reset_start_time_i2_m2 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4.
intros.
intro; intros.
elim H12.
intro.
elim H13; intros.
 rewrite (h_m2 c) in |- *; split.
  left; repeat split.
    generalize reset_start_time_t1_remain_false; intros.
    red in H15.
     eapply H15.
     apply H.
    auto.
    auto.
    auto.
    apply H3.
    auto.
    auto.
    auto.
    generalize reset_start_exceed_time_t1_m5_false_general; intros.
    cut (pred c = c2 \/ pred c <> c2); intros.
     elim H16; intros.
    rewrite H17 in |- *.
      generalize reset_no_start_m5; intros.
      red in H18.
       eapply H18.
       apply H0.
      apply H1.
      auto.
      eapply H15.
      apply H.
     auto.
     auto.
     auto.
      omega.
     auto.
     auto.
     auto.
     auto.
     red in |- *; intros.
     elim_clear H18.
      eapply H11.
      omega.
   omega.
   generalize reset_start_noreset_m1; intros.
   red in H15.
    eapply H15.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
  rewrite (h_m2 (S m)) in |- *; repeat split.
 simpl in |- *.
   right.
   apply H15.
    omega.
generalize reset_start_noreset_m1; intros.
  red in H17.
   eapply H17.
   apply H0.
  apply H1.
  auto.
  apply H11.
   omega.
Qed.

Lemma reset_start_time_i2_m5 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m5 c c4.
intros.
cut (being_true m2 c c4); intros.
 intro.
   intros.
   rewrite (h_m5 c0) in |- *; try split.
  left.
    left.
    apply H12; auto.
 generalize reset_start_noreset_m1; intros.
   red in H14.
    eapply H14.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
   eapply reset_start_time_i2_m2.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.



Lemma reset_start_time_i2_o0 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4.
intros.
cut (being_false o0 (S c2) c /\ being_false o0 c c4); intros.
 elim_clear H12.
   intro; intros.
   red in H13; red in H14.
   cut (c0 < c \/ c <= c0); intros.
    elim H15; intros.
   apply H13.
      omega.
  apply H14;  omega.
  omega.
  split.
 intro; intros.
   rewrite (h_o0 c0) in |- *; red in |- *; intros.
   elim_clear H13.
   generalize reset_start_time_t1_remain_false; intros.
   red in H13; red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   cut (S c2 <= c0 <= c3); intros.
    apply H16.
    omega.
   auto.
  intro; intros.
  rewrite (h_o0 c0) in |- *; red in |- *; intros.
  elim_clear H13.
  generalize reset_start_time_i2_m5; intros.
  red in H13.
  apply H15.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  intro; intros.
  red in H7.
  apply H7;  omega.
  intro; intros; red in H8; apply H8;  omega.
  auto.
  apply H10.
  auto.
   omega.
Qed.

Lemma reset_start_time_i2_i3i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4 /\ being_false m3 c c4 /\ being_false m4 c c4.
repeat split.
  eapply (reset_start_time_i2_m2 c1 c2 H H0 H1 H2 c3); auto.
  intro; intros.
    apply H7;  omega.
 intro; intros.
   apply H8;  omega.
intro; intros.
  elim H12; intro.
  elim H13; intros.
 rewrite (h_m3 c) in |- *; red in |- *; intros.
   elim_clear H15.
   elim_clear H16.
  elim_clear H15.
    elim_clear H18.
    red in H7; red in H7.
     eapply (H7 c); auto.
     omega.
 cut (S c2 = c \/ S c2 < c); intros.
  elim_clear H16.
   rewrite <- H18 in *; simpl in *.
     generalize reset_no_start_m3; intros.
     red in H16; red in H16.
      eapply H16.
      apply H0.
     apply H1.
     cut (c1 <= c2 <= c2); intros; try  omega.
     apply H19.
     auto.
    generalize reset_start_noi3_nom3; intros.
    red in H16; red in H16;  eapply H16.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < c); intros.
     apply H19.
    omega.
    auto.
    cut (S c2 <= pred c <= c); intros.
     apply H19.
     omega.
    auto.
    omega.
  rewrite (h_m3 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H17.
  elim_clear H18.
 elim_clear H17.
   elim_clear H20.
   apply H21.
   generalize reset_start_time_i2_m5; intros.
   red in H20.
    eapply H20.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   red in H7.
   intro; intros.
   apply H7.
    omega.
   red in H8.
   intro; intros.
   apply H8.
    omega.
   auto.
   apply H10.
   auto.
    omega.
  apply H15.
  omega.
auto.
  intro; intros.
  elim H12; intro.
  elim H13; intros.
 rewrite (h_m4 c) in |- *; red in |- *; intros.
   elim_clear H15.
   elim_clear H16.
  elim_clear H15.
    elim_clear H18.
    red in H8; red in H8.
     eapply (H8 c); auto.
     omega.
 cut (S c2 = c \/ S c2 < c); intros.
  elim_clear H16.
   rewrite <- H18 in *; simpl in *.
     generalize reset_no_start_m4; intros.
     red in H16; red in H16.
      eapply H16.
      apply H0.
     apply H1.
     cut (c1 <= c2 <= c2); intros; try  omega.
     apply H19.
     auto.
    generalize reset_start_noi4_nom4; intros.
    red in H16; red in H16;  eapply H16.
     apply H.
    auto.
    auto.
    auto.
    cut (c2 < c); intros.
     apply H19.
     omega.
    auto.
    cut (S c2 <= pred c <= c); intros.
     apply H19.
     omega.
    auto.
    omega.
  rewrite (h_m4 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H17.
  elim_clear H18.
 elim_clear H17.
   elim_clear H20.
   apply H21.
   generalize reset_start_time_i2_m5; intros.
   red in H20.
    eapply H20.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   red in H7.
   intro; intros.
   apply H7.
    omega.
   red in H8.
   intro; intros.
   apply H8.
    omega.
   auto.
   apply H10.
   auto.
    omega.
  apply H15.
  omega.
auto.
Qed.

Lemma reset_start_time_i2_m3m4 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m2 c c4 /\ being_false m2 (S c2) (pred c) /\ being_false m3 (S c2) c4 /\ being_false m4 (S c2) c4.
intros.
generalize
 (reset_start_time_i2_i3i4disabled c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9
    c4 H10 H11); intros.
elim_clear H12.
elim_clear H14.
repeat split.
 auto.
intro.
  intros.
  generalize reset_start_noi2_nom2; intros.
  red in H16.
   eapply H16.
   apply H.
  auto.
  auto.
  auto.
  cut (c2 < pred c); intros.
   apply H17.
   omega.
  auto.
  omega.
  assert (being_false m3 (S c2) c).
  eapply reset_start_noi3_nom3.
    apply H.
   auto.
   auto.
   auto.
    omega.
   auto.
  red in |- *; intros.
  cut (c0 < c \/ c <= c0); intros.
   elim_clear H17.
  red in H14.
    apply H14; auto.
     omega.
 red in H12.
   apply H12;  omega.
 omega.
  assert (being_false m4 (S c2) c).
 generalize reset_start_noi4_nom4; intros.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
    omega.
   auto.
  red in |- *; intros.
  cut (c0 < c \/ c <= c0); intros.
   elim_clear H17.
  red in H14.
    apply H14; auto.
     omega.
 red in H15.
   apply H15;  omega.
 omega.
Qed.





Lemma reset_start_time_i2_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) c ->
            being_false i4 (S c2) c ->
            i2 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4 /\
                being_true o1 c c4 /\ 
                being_false o1 (S c2) (pred c) /\ 
                being_false o2 (S c2) c4 /\ 
                being_false o3 (S c2) c4.
intros.
split.
 generalize
  (reset_start_time_i2_o0 c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9 c4 H10
     H11).
   auto.
generalize
 (reset_start_time_i2_m3m4 c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8 H9 c4 H10
    H11); intros.
  elim_clear H12.
  elim_clear H14.
  elim_clear H15.
  repeat split.
 red in |- *; intros.
   rewrite (h_o1 c0) in |- *.
   apply H13; auto.
red in |- *; intros.
  rewrite (h_o1 c0) in |- *; intros.
  apply H12; auto.
red in |- *; intros.
  rewrite (h_o2 c0) in |- *; intros.
  apply H14; auto.
red in |- *; intros.
  rewrite (h_o3 c0) in |- *; intros.
  apply H16; auto.
Qed.

Lemma reset_start_time_i3_m3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) (pred c) ->
            i3 c -> 
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true m3 c c4.
intros.
intro; intros.
elim H12.
intro.
elim H13; intros.
 rewrite (h_m3 c) in |- *; split.
  left; repeat split.
    generalize reset_start_time_t1_remain_false; intros.
    red in H15.
     eapply H15.
     apply H.
    auto.
    auto.
    auto.
    apply H3.
    auto.
    auto.
    auto.
    generalize reset_start_exceed_time_t1_m5_false_general; intros.
    cut (pred c = c2 \/ pred c <> c2); intros.
     elim H16; intros.
    rewrite H17 in |- *.
      generalize reset_no_start_m5; intros.
      red in H18.
       eapply H18.
       apply H0.
      apply H1.
      auto.
      eapply H15.
      apply H.
     auto.
     auto.
     auto.
      omega.
     auto.
     auto.
     auto.
     auto.
     red in |- *; intros.
     elim_clear H18.
      eapply H11.
      omega.
   omega.
   generalize reset_start_noreset_m1; intros.
   red in H15.
    eapply H15.
    apply H0.
   apply H1.
   auto.
   apply H11.
    omega.
  rewrite (h_m3 (S m)) in |- *; repeat split.
 simpl in |- *.
   right.
   apply H15.
    omega.
generalize reset_start_noreset_m1; intros.
  red in H17.
   eapply H17.
   apply H0.
  apply H1.
  auto.
  apply H11.
   omega.
Qed.

Lemma reset_start_time_m5enabled_i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i4 (S c2) c ->
            forall c4, c <= c4 -> 
                being_true m5 c c4 ->
                being_false i1 (S c2) c4 ->
                being_false m4 c c4.
intros.
cut (~ m4 c); intros.
 intro; intros.
   elim H11; intro.
   elim H12; intros.
  auto.
 rewrite (h_m4 (S m)) in |- *; simpl in |- *; red in |- *; intros.
   elim_clear H16.
   elim_clear H17.
    elim_clear H16.
    elim_clear H19.
    apply H20.
    apply H8;  omega.
 apply H14; auto.
    omega.
  cut (being_false m4 (S c2) c); intros.
 apply H10;  omega.
 eapply reset_start_noi4_nom4.
   apply H.
  auto.
  auto.
  auto.
   omega.
  auto.
Qed.

Lemma reset_start_time_i2i3_i4disabled : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                
                being_false m2 (S c2) (pred c) /\
                being_true m2 c c4 /\ 
                being_false m3 (S c2) (pred c) /\
                being_true m3 c c4 /\ 
                being_false m4 (S c2) c4.
repeat split.
 generalize reset_start_noi2_nom2; intros.
   intro; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (S c2 <= pred c); intros.
    red in |- *.
    apply H15.
    omega.
   auto.
   auto.
   eapply reset_start_time_i2_m2.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
  apply H8; auto.
   omega.
  auto.
  auto.
  auto.
  generalize reset_start_noi3_nom3; intros.
  red in H13.
  intro; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  cut (S c2 <= pred c); intros.
   red in |- *.
   apply H15.
   omega.
  auto.
  auto.
  generalize reset_start_time_i3_m3; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
  apply H8; auto.
   omega.
  auto.
  auto.
  auto.
  cut (being_false m4 (S c2) c /\ being_false m4 c c4); intros.
 elim_clear H13.
   intro; intros.
   cut (c0 < c \/ c <= c0); intros.
  elim_clear H16.
   apply H14;  omega.
  apply H15;  omega.
  omega.
split.
 intro; intros.
   generalize reset_start_noi4_nom4; intros.
   red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   cut (S c2 <= c); intros.
    red in |- *; apply H15.
    omega.
   auto.
    omega.
  generalize reset_start_time_m5enabled_i4disabled; intros.
  red in H13.
  intro; intros.
   eapply H13.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  apply H11.
  auto.
  generalize reset_start_time_i2_m5; intros.
   eapply H15.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  intro; intros.
   eapply H8; auto.
   omega.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_time_i2i3_o0 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) c4.
intros.
intros.
cut (being_false o0 (S c2) c /\ being_false o0 c c4); intros.
 elim_clear H13.
   intro; intros.
   red in H14; red in H15.
   cut (c0 < c \/ c <= c0); intros.
  elim H16; intros.
   apply H14.
      omega.
  apply H15;  omega.
  omega.
split.
 intro; intros.
   rewrite (h_o0 c0) in |- *; red in |- *; intros.
   elim_clear H14.
   generalize reset_start_time_t1_remain_false; intros.
   red in H14; red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   cut (S c2 <= c0 <= c3); intros.
    apply H17.
    omega.
   auto.
  intro; intros.
  rewrite (h_o0 c0) in |- *; red in |- *; intros.
  elim_clear H14.
  generalize reset_start_time_i2_m5; intros.
  red in H14.
  apply H16.
   eapply H14.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  apply H5.
  auto.
  auto.
  red in |- *; intros; red in H8; apply H8;  omega.
  auto.
  apply H11.
  auto.
   omega.
Qed.

Lemma reset_start_time_i2i3_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c, 
            S c2 <= c <= c3 ->
            being_false i2 (S c2) (pred c) ->
            being_false i3 (S c2) (pred c) ->
            being_false i4 (S c2) c ->
            i2 c -> 
            i3 c ->
            forall c4, c <= c4 -> 
                being_false i1 (S c2) c4 ->
                
                being_false o0 (S c2) c4 /\
                being_true o1 c c4 /\ 
                being_false o1 (S c2) (pred c) /\ 
                being_true o2 c c4 /\ 
                being_false o2 (S c2) (pred c) /\ 
                being_false o3 (S c2) c4.
intros.
split.
  eapply reset_start_time_i2i3_o0.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H5.
   auto.
   auto.
   auto.
   auto.
   auto.
   auto.
   auto.
  generalize
   (reset_start_time_i2i3_i4disabled c1 c2 H H0 H1 H2 c3 H3 H4 c H5 H6 H7 H8
      H9 H10 c4 H11 H12); intros.
  elim_clear H13.
  elim_clear H15.
  elim_clear H16.
  elim_clear H17.
  repeat split.
 intro; intros.
   rewrite (h_o1 c0) in |- *; intros.
    eapply H13; auto.
intro; intros.
  rewrite (h_o1 c0) in |- *; intros.
   eapply H14; auto.
intro; intros.
  rewrite (h_o2 c0) in |- *; intros.
   eapply H16; auto.
intro; intros.
  rewrite (h_o2 c0) in |- *; intros.
   eapply H15; auto.
intro; intros.
  rewrite (h_o3 c0) in |- *; intros.
   eapply H18; auto.
Qed.

Lemma reset_start_exceed_time_t1 : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3, 
            t1_PT <= f (pred c3) - f c2 -> 
            being_false i1 (S c2) c3 ->
            t1 c3.  
intros.
intros.
cut (being_true m1 (S c2) c3); intros.
  eapply h_t1_set.
    cut (m1 (S c2)); intros.
cut (t1_PT <= f(pred c3) - f (pred (S c2)));intros.
apply H6.
simpl;auto.
    apply H4.
    split; auto.
    cut (f c2 < f (pred c3)); intros.
   generalize (f_2 c2 (pred c3)); intros.
      omega.
  cut (1 <= t1_PT); try  omega.
    apply t1_LargerThan0.
   auto.
  auto.
   eapply reset_start_noreset_m1.
   apply H.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_strong : 
    forall c1 c2, i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_true t1 (S (S c3)) c4.    
intros.
intro; intros.
 eapply reset_start_exceed_time_t1.
   apply H.
  apply H0.
  auto.
  cut (f (S c3) <= f (pred c)); intros.
omega.
cut (S c3 = pred c \/ S c3 < pred c); intros; try  omega.
  elim H7; intros.
 rewrite H8 in |- *; auto.
cut (f (S c3) < f (pred c)); intros; try  omega.
  apply f_1; auto.
  intro; intros.
  apply H5.
   omega.
Qed.

Lemma reset_start_exceed_time_t1_m2_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m2 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m2 (S c3)); intros.
  rewrite (h_m2 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi2_nom2; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m2 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m2_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m2 (S c2) c4.   
intros.
intros.
cut (being_false m2 (S c2) (S c3)); cut (being_false m2 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m2_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi2_nom2.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m2_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m3_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i3 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m3 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m3 (S c3)); intros.
  rewrite (h_m3 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi3_nom3; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m3 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m3_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i3 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m3 (S c2) c4.   
intros.
intros.
cut (being_false m3 (S c2) (S c3)); cut (being_false m3 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m3_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi3_nom3.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m3_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m4_false_1 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m4 (S (S c3)) c4.   
intros.
intro.
intro.
elim H8; intro.
elim H8; intro.
elim H9; intros.
 cut (~ m4 (S c3)); intros.
  rewrite (h_m4 (S (S c3))) in |- *; red in |- *; simpl in |- *; intros.
    elim_clear H14.
    elim_clear H15.
   elim_clear H14.
     elim_clear H17.
     cut (t1 (S (S c3))); auto.
      eapply reset_start_exceed_time_t1.
      apply H0.
     apply H1.
     auto.
     auto.
     auto.
     red in |- *; intros.
     apply H7;  omega.
    auto.
   generalize reset_start_noi4_nom4; intros.
   red in H13.
    eapply H13.
    apply H.
   auto.
   auto.
   auto.
   cut (c2 < (S c3)); intros.
    apply H14.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
   intro.
   intros.
   apply H5.
   omega.
   split; auto.
   cut (c2 < S c3); try  omega.
   cut (f c2 < f (S c3)); intros; try  omega.
   generalize (f_2 _ _ H14); intros; try  omega.
  rewrite (h_m4 (S m)) in |- *; red in |- *; intros; simpl in *.
  elim_clear H15.
  elim_clear H16.
 cut (t1 (S m)); intros; try  tauto.
   generalize reset_start_exceed_time_t1_strong.
   intros.
   red in H16.
    eapply H16.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H6.
   auto.
   auto.
  apply H12; auto.
  omega.
 omega.
Qed.   
 
Lemma reset_start_exceed_time_t1_m4_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m4 (S c2) c4.   
intros.
intros.
cut (being_false m4 (S c2) (S c3)); cut (being_false m4 (S (S c3)) c4); intros; auto.
 intro; intros.
   cut (S (S c3) <= c \/ S (S c3) > c); intros.
  elim H11; intros.
   apply H8; auto.
      omega.
  apply H9; try  omega.
  omega.
 eapply reset_start_exceed_time_t1_m4_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_noi4_nom4.
   apply H.
  auto.
  auto.
  auto.
  cut (f c2 < f (S c3)); try  omega.
  intros.
  apply f_2; auto.
intro.
intros.
apply H5;omega.
   eapply reset_start_exceed_time_t1_m4_false_1.
   apply H.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
  auto.
Qed.


Lemma reset_start_exceed_time_o123 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o1 (S c2) c4 /\ being_false o2 (S c2) c4 /\ being_false o3 (S c2) c4.
repeat split.
 cut (being_false m2 (S c2) c4); intros.
  intro; intros.
    rewrite h_o1 in |- *; intros.
    apply H10; auto.
  eapply reset_start_exceed_time_t1_m2_false.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   auto.
   auto.
   auto.
  cut (being_false m3 (S c2) c4); intros.
 intro; intros.
   rewrite h_o2 in |- *; intros.
   apply H10; auto.
 eapply reset_start_exceed_time_t1_m3_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  cut (being_false m4 (S c2) c4); intros.
 intro; intros.
   rewrite h_o3 in |- *; intros.
   apply H10; auto.
 eapply reset_start_exceed_time_t1_m4_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_exceed_time_t1_m5_false : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false m5 (S c2) c4.   
intros.
cut
 (being_false m2 (S c2) c4 /\
  being_false m3 (S c2) c4 /\ being_false m4 (S c2) c4);
 intros.
 elim_clear H10.
   elim_clear H12.
   intro; intros.
   elim H12; intro.
   elim_clear H14.
  rewrite (h_m5 (S c2)) in |- *; red in |- *; intros.
    elim_clear H14.
    elim_clear H16.
   elim_clear H14.
    red in H11; red in H11.
       eapply H11; auto.
     elim_clear H16.
    red in H10; red in H10.
       eapply H10; auto.
     red in H13; red in H13.
      eapply H13; auto.
    simpl in *.
    generalize reset_no_start_m5; intros.
    red in H16; red in H16.
     eapply H16.
     apply H0.
    apply H1.
    cut (c1 <= c2 <= c2); intros.
     apply H18.
     omega.
    auto.
   rewrite (h_m5 (S m)) in |- *; red in |- *; intros.
   elim_clear H14.
   elim_clear H18.
  elim_clear H14.
   red in H11; red in H11.
      eapply H11; auto.
      cut (S c2 <= S m <= c4); intros; try  omega.
      apply H14.
     auto.
    elim_clear H18.
   red in H10; red in H10.
      eapply H10; auto.
      cut (S c2 <= S m <= c4); intros; try  omega.
      apply H18.
     auto.
    red in H13; red in H13.
     eapply H13; auto.
     cut (S c2 <= S m <= c4); intros; try  omega.
     apply H18.
    auto.
   simpl in H14.
   apply H16; try  omega; auto.
  repeat split.
  eapply reset_start_exceed_time_t1_m2_false.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   auto.
   auto.
   auto.
   eapply reset_start_exceed_time_t1_m3_false.
   apply H.
  auto.
  apply H1.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
   eapply reset_start_exceed_time_t1_m4_false.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
Qed.

Lemma reset_start_time_t1_remain_false_strong:
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false t1 (S c2) (S c3).
intros.
intro.
intros.
red in |- *; intros.
generalize (h_t1_true _ H6); intros.
elim_clear H7.
elim_clear H8.
generalize (reset_no_start_m1 c1 c2 H0 H1); intros.
red in H8; red in H9; red in H8.
generalize (H9 c2); intros.
generalize (H8 c2); intros.
cut (x <= c2 <= c /\ c1 <= c2 <= c2); intros.
 elim H12; auto.
split;auto.
split.
Focus 2.
elim H5;omega.
   cut (x <= c2 \/ c2 < x); intros.
Focus 2.
omega.
    elim H12; intros; auto.
assert (f (pred c) - f (pred x) < t1_PT).
eapply  (f_3_inner c2 (pred x) (pred c) c3 t1_PT).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12.
try omega.
cut (f (pred x) < f (pred c));intros.
g_intro ( f_2 (pred x) (pred c) H14).
clear H H0 H1 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14.
omega.
clear H H0 H1 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
clear H H0 H1 H3 H4 H6 H7 H8 H9 H10 H11 H12 H13.
omega.
auto.
clear H H0 H1 H3 H4 H5 H6 H8 H9 H10 H11 H12 H13.
omega.
Qed.


Lemma reset_start_exceed_time_o0o1o2o3 : 
    forall c1 c2, c1 <= c2 -> i1 c1 -> being_false i0 c1 c2 ->
        i0 (S c2) ->
        forall c3,
            f c3 - f c2 < t1_PT -> 
            t1_PT <= f (S c3) - f c2 ->
            being_false i2 (S c2) (S (S c3)) ->
            being_false i3 (S c2) (S (S c3)) ->
            being_false i4 (S c2) (S (S c3)) ->
            forall c4, S (S c3) <= c4 -> 
                being_false i1 (S c2) c4 ->
                being_false o0 (S c2) (S c3) /\ being_true o0 (S (S c3)) c4 /\
                being_false o1 (S c2) c4 /\ 
                being_false o2 (S c2) c4 /\ 
                being_false o3 (S c2) c4.
intros.
generalize
 (reset_start_exceed_time_o123 c1 c2 H H0 H1 H2 c3 H3 H4 H5 H6 H7 c4 H8 H9);
 intros.
elim_clear H10.
elim_clear H12.
repeat split; auto.
 red in |- *; intros.
   rewrite (h_o0 c) in |- *; red in |- *; intros.
   elim_clear H14.
   generalize reset_start_time_t1_remain_false_strong; intros.
   red in H14; red in H14.
    eapply H14.
    apply H.
   auto.
   auto.
   auto.
   apply H3.
   auto.
   apply H12.
   auto.
  red in |- *; intros.
  rewrite (h_o0 c) in |- *; intros.
  split.
 generalize reset_start_exceed_time_t1_strong; intros.
   red in H14.
    eapply H14.
    apply H0.
   apply H1.
   auto.
   apply H3.
   auto.
   apply H8.
   auto.
   auto.
  generalize reset_start_exceed_time_t1_m5_false; intros.
  red in H14.
   eapply H14.
   apply H.
  auto.
  auto.
  auto.
  apply H3.
  auto.
  auto.
  auto.
  auto.
  apply H8.
  auto.
  auto.
  cut (c2 < S c3); intros; try  omega.
  cut (f (c2) < f (S c3)); intros.
 apply f_2; auto.
 omega.         
Qed.


(*****************************************************************************)

(*final theorem for play press only*)

Definition reset_then_start c1 c2 := c1 <= c2 /\ i1 c1 /\ i0 (S c2) /\ being_false i0 c1 c2.
Definition just_time_out c1 c2 := t1_PT <= f (S c2) - f c1 /\ f c2 - f c1 < t1_PT. 
Definition p1_first_presses c1 c2 := being_false i2 c1 (pred c2) /\ being_false i3 c1 c2 /\ being_false i4 c1 c2 /\ i2 c2.
Definition p1p2_first_press c1 c2 := being_false i2 c1 (pred c2) /\ being_false i3 c1 (pred c2) /\ being_false i4 c1 c2 /\ i2 c2 /\ i3 c2.
Definition no_player_press c1 c2 := being_false i2 c1 c2 /\ being_false i3 c1 c2 /\ being_false i4 c1 c2.
Definition not_reset c1 c2 := being_false i1 c1 c2.
Definition off_on o c1 c2 c3 := being_true o c2 c3 /\ being_false o c1 (pred c2).
Definition stay_off o c1 c2 := being_false o c1 c2.


Theorem reset_start_time_i2_o0o1o2o3_f : 
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out c2 c3 ->
            forall c, 
            S c2 <= c <= c3 -> p1_first_presses (S c2) c -> 
            forall c4, c <= c4 -> 
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                stay_off o2 (S c2) c4 /\
                stay_off o3 (S c2) c4.
intros.
unfold stay_off in |- *; unfold off_on in |- *; unfold reset_then_start in *;
 unfold just_time_out in *; unfold p1_first_presses in *;
 unfold not_reset in *.
cut
 (being_false o0 (S c2) c4 /\
  being_true o1 c c4 /\
  being_false o1 (S c2) (pred c) /\
  being_false o2 (S c2) c4 /\ being_false o3 (S c2) c4);
 try  tauto.
elim_clear H.
elim_clear H6.
elim_clear H7.
elim_clear H0.
elim_clear H2.
elim_clear H10.
elim_clear H11.
 eapply (reset_start_time_i2_o0o1o2o3 c1); auto.
   apply H9.
  auto.
  auto.
Qed.

(*final theorem for play 1 and player 2 press at exactly the same time*)

Theorem reset_start_time_i2i3_o0o1o2o3_f : 
    forall c1 c2, reset_then_start c1 c2 ->
        forall c3,
            just_time_out c2 c3 ->
            forall c, 
            S c2 <= c <= c3 ->
            p1p2_first_press (S c2) c ->
            forall c4, c <= c4 -> 
                not_reset (S c2) c4 ->
                stay_off o0 (S c2) c4 /\
                off_on o1 (S c2) c c4 /\
                off_on o2 (S c2) c c4 /\
                stay_off o3 (S c2) c4.
intros.
unfold stay_off in |- *; unfold off_on in |- *; unfold reset_then_start in *;
 unfold just_time_out in *; unfold p1_first_presses in *;
 unfold not_reset in *.
cut
 (being_false o0 (S c2) c4 /\
  being_true o1 c c4 /\
  being_false o1 (S c2) (pred c) /\
  being_true o2 c c4 /\
  being_false o2 (S c2) (pred c) /\ being_false o3 (S c2) c4);
 try  tauto.
elim_clear H.
elim_clear H6.
elim_clear H7.
elim_clear H0.
elim_clear H2.
elim_clear H10.
elim_clear H11.
elim_clear H12.
 eapply (reset_start_time_i2i3_o0o1o2o3 c1); auto.
   apply H9.
  auto.
  auto.
Qed.







